\documentclass[xcolor=pdftex,dvipsnames]{beamer}
\usepackage{beamerthemesplit}


\makeatletter

\usefoottemplate{%
  \vbox{\tiny%
  \hbox{%
  \setbox\beamer@linebox=\hbox to\paperwidth{%
    \hbox to.5\paperwidth{\hfill\tiny\color{white}\textbf{\insertshortauthor}\hskip.3cm}%
    \hbox to.5\paperwidth{\hskip.3cm\tiny\color{white}\textbf{\insertshorttitle}\hfill\textbf{\insertframenumber/\inserttotalframenumber}\hspace{.3cm}}\hfill}%
  \ht\beamer@linebox=2.625ex%
  \dp\beamer@linebox=0pt%
  \setbox\beamer@linebox=\vbox{\box\beamer@linebox\vskip1.125ex}%
  \color{black}\hskip-\Gm@lmargin\vrule width.5\paperwidth
  height\ht\beamer@linebox\color{structure}\vrule width.5\paperwidth
  height\ht\beamer@linebox\hskip-\paperwidth% 
  \hbox{\box\beamer@linebox\hfill}\hfill\hskip-\Gm@rmargin}}}

\usetitlepagetemplate{
    \vbox{}
    \vfill
    \begin{centering}
      \Large\structure{\inserttitle}
      \vskip1em\par
      \large\insertauthor\vskip1em\par
      {\normalsize\insertinstitute\par}\par\vskip1em
      \insertdate\par\vskip1.5em
      \inserttitlegraphic\par
    \end{centering}
    \vfill
  }
\makeatother





%\usetheme{Fabian}
\beamertemplatenavigationsymbolsempty

\definecolor{myGreen}{HTML}{006C35}

\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb}
\usepackage{graphicx,color}
\usepackage{pgfplots}
\usepackage{hyperref}

\usetikzlibrary{calc}

\pgfplotsset{compat=1.3}

\date{17th April 2014}


\newcommand<>{\emp}[1]{{\only#2{\color{red}}#1}}
\newcommand{\inter}[2]{\left( #1, #2\right]}
\newcommand{\nat}{\mathbb{N}}

\newcommand{\sd}[1]{#1}
\newcommand{\ld}[1]{\raisebox{-1ex}[0cm][0cm]{\sd{#1}}}
\newcommand{\ud}[1]{\raisebox{1ex}[0cm][0cm]{\sd{#1}}}
\newcommand{\ub}[1]{\raisebox{1ex}[0cm][0cm]{#1}}
\newcommand{\LPBT}[2]{}%\mathit{I}(#1,#2)\equiv}
\newcommand{\threshold}[2]{(#1,#2]}

%\setbeamercolor{block title example}{fg=white,bg=myGreen}
%\setbeamercolor{block title}{fg=white,bg=myGreen}

\title[Threshold Synthesis Problem]{Implementations of two Algorithms for the Threshold Synthesis Problem}
\author[Smaus, Schilling, Wenzelmann]{\textbf{Jan-Georg Smaus}\inst{1}
  \\ \and Christian Schilling\inst{2} \and Fabian Wenzelmann\inst{2}}
\institute[]
{
\inst{1}
IRIT\and
\inst{2}
Institut f\"ur Informatik\\
Albert-Ludwigs-Universit\"at Freiburg\\
Germany
}

\keywords{Boolean function, threshold logic, FAC2014, logic, computer science, algorithm, mathematics, linear programming}
\subject{Implementations of two Algorithms for the Threshold Synthesis Problem: Presentation}

\newcommand{\OP}{\mathit{OP}}
\newcommand{\ms}[1]{\{\hspace{-0.2em}[#1]\hspace{-0.2em}\}}
\newcommand{\Cut}[3]{\mathit{S}(#1,#2,#3)}
\newcommand{\CutT}[2]{\mathit{S}(\cdot,#1,#2)}

\newcommand{\splitD}[3]{\mathit{S}\left( #1, #2, #3 \right)}
\newcommand{\splitA}[2]{\splitD{\cdot}{#1}{#2}}
\newcommand{\splitAV}[3]{\splitA{ x_{#1 \dots #2} } {#3} }

\newcommand{\false}{\mathit{false}}
\newcommand{\true}{\mathit{true}}

\newcommand{\falseInt}[1]{\inter{#1}{\infty}}
\newcommand{\trueInt}{\inter{-\infty}{0}}

\newcommand{\mmi}[1]{\left( #1 \right]}
\newcommand{\br}[1]{\left( #1 \right)}

%\renewcommand{\emph}[1]{\textcolor{blue}{\textit{#1}}}
\newcommand{\emf}[1]{\textcolor{blue}{#1}}

\pgfdeclarelayer{background}
\pgfdeclarelayer{foreground}
\pgfsetlayers{background,main,foreground}

\definecolor{shadecolor}{rgb}{.9,.9,1}

\def\naive{na\"{\i}ve}

\begin{document}
\begin{frame}
\titlepage
\end{frame}


%\begin{frame}
%\frametitle{Contents}
%\tableofcontents
%\end{frame}


%\section{Problem Definition}

\begin{frame}
\frametitle{Linear Pseudo-Boolean Constraints}

\textbf{Context}: Propositional logic \pause

\medskip

\textbf{Definition}: A \emp{linear pseudo-Boolean constraint} is
\begin{align*}
a_1\cdot \ell_1+\ldots+a_m\cdot \ell_m\geq d
\qquad a_i,d\in\nat,\ell_i\in\{x_i,\bar{x}_i\equiv1-x_i\}.
\end{align*}

\pause

\begin{itemize}
\item LPBs represent Boolean functions: $Bool^m\to Bool$.
\item Boolean functions that can be represented by a \emf{single} LPB are called \emf{threshold functions}.
\item The problem of finding a single LPB representing a DNF $\phi$ is called \emf{threshold synthesis problem}.
% TODO: schon sehr viel Text
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Linear Pseudo-Boolean Constraints: Example}

The DNF $\phi \equiv x_1 \lor \left(x_2 \land x_3\right)$ can be represented by $2x_1 + x_2 + x_3 \geq 2$.

\begin{figure}
\centering
\scalebox{0.9}{
\begin{tikzpicture}
\begin{axis}
[
xlabel=$x_1$,
ylabel=$x_2$,
zlabel=$x_3$,
xlabel style={sloped like x axis},
ylabel style={sloped like y axis},
zlabel style={sloped like z axis},
view={-25}{45},
xtick=data,
ytick=data,
ztick=data,
zmin=0,
anchor=center,
%enlarge z limits=false
]
\addplot3[only marks, blue, mark=square*, fill=green, domain=0:1] file {plots/true_points.dat};
\addplot3[only marks, red, domain=0:1] file {plots/false_points.dat};
\addplot3[mesh,draw=orange, samples=10, domain=0:1] { 2-2*x-y};
\end{axis}
\end{tikzpicture}}
\end{figure}
% TODO: sinnvoll? f\"ur die anschaung eigentlich ganz gut so was zu sehen
% sollte man dann noch etwas dazu schreiben?

\end{frame}


\begin{frame}
\frametitle{Background}
Applications in 
\begin{itemize}
\item Artificial intelligence \cite{BarBoc93} 
\item Electronic design automation \cite{ChaKue03}
\item Game theory \cite{Bol11OR} \ldots \pause
\end{itemize}

\bigskip

We present \emp{implementations} of two algorithms for the problem
with an experimental evaluation.  
\end{frame}


% TODO: sollte man sich hier an die Gro\ss schreibkonventionen f\"ur Titel halten (im Paper nicht...)
\section{The Linear Programming Algorithm}

\begin{frame}
\frametitle{Linear Programming Algorithm}
We make use of the \emf{minimal true points} and \emf{maximal false points} of the DNF.
\begin{itemize}
\item Minimal true points: obvious from the DNF.
\item Maximal false points: not obvious, but can be computed in polynomial time.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Linear Programming Algorithm: The Linear Program}
% TODO: nur wegen irredu was auch immer?
\begin{itemize}
\item Given the minimal true points $x^1, \dots, x^k$ and
\item maximal false points $y^1, \dots, y^\ell$ 
\end{itemize}
the linear program is:
\begin{alignat}{8}
	\sum_{i=1}^m a_i x_i^j &\quad& \geq &\quad&& d &\quad& (1 \leq j \leq k) \\
	\sum_{i=1}^m a_i y_i^j && < &&& d && (1 \leq j \leq \ell) \\
	a_i && \geq &&& 0 && (1 \leq i \leq m)
\end{alignat}
\emf{Note:} The $a_i$ and $d$ are the \emf{variables} of the linear program.
% TODO: the other parts? was f\"ur other parts? (im paper)

Runtime: $O(m^7t^5)$.
\end{frame}

\section{The Combinatorial Algorithm}

\begin{frame}
\frametitle{Combinatorial Algorithm}
\begin{itemize}
\item 
\emph{Combinatorial algorithm}: Considered a challenge by
\cite{CraHam11} although an algorithm has been proposed by
\cite{CoaLew61}, later reinvented by \cite{Sma-CPAIOR07}. 
\item It turned out that the basic 
combinatorial algorithm is \emp{not complete} \cite{WenzelmannBachelor11}. 
Partial remedy proposed here \ldots
\end{itemize}
\end{frame}

\subsection{Preliminaries}
\begin{frame}
\frametitle{Variable Order}
Before determining the coefficients for the variables, one can first
determine an \emp{ordering} : 
A variable has much weight if it occurs in \emp{many} clauses and if it occurs
in \emp{short} clauses. 

\bigskip

\textbf{Example}
\[
\begin{array}{l}
(x_1\land x_2)\lor(x_1\land x_3)\lor(x_1\land x_4)\lor(x_1\land x_5)\\
\lor(x_2\land x_3)\lor
(x_2\land x_4)\lor(x_3\land x_4\land x_5)  
\end{array}
\]
\\

$x_1$ occurs in 4 clauses of length 2.\\
$x_2$ occurs in 3 clauses of length 2.\\
$x_3$ occurs in 3 clauses, 2 of length 2 and 1 of length 3.\\

\smallskip

Hence $x_1 \succeq x_2\succeq x_3$. 
\end{frame}


\begin{frame}{Modus Operandi}
\begin{enumerate}
\item Find the maximal $\ell$ such that $x_1,\dots,x_\ell$ are all equivalent wrt.~$\succeq$ (Possibly $\ell=1$).
%	\item Test if all these variables are pairwise symmetric.
	\item \emf{Split} away the variables and obtain sub-problems.
	\item Solve the sub-problems recursively.
\end{enumerate}
\end{frame}


\begin{frame}{Minimum and Maximum Degree}
Given an LPB $I \equiv \sum_{i=1}^m a_ix_i \geq d$, it is possible to shift $d$
to some extent without changing the meaning. \pause

We introduce the notation
\begin{align*}
\sum\limits_{i=1}^m a_i x_i \geq \inter{s}{b}
\end{align*}
if for each $d' \in \inter{s}{b}$ the LPB $\sum_{i=1}^m a_ix_i \geq d'$ 
represents the same Boolean function as $I$.

We allow $s = -\infty$ and $b = \infty$.
\end{frame}


\subsection{Decomposing a DNF and Composing LPBs}

\begin{frame}
\frametitle{Decomposing a DNF}

\begin{center}
\hspace*{-10mm}
\scalebox{0.85}
{
\begin{tikzpicture}[node distance=.25cm, every node/.style={anchor=west}]
\def\rS{0}
\def\distance{0.55cm}

\uncover<4->
{
\node at (\rS, 0) (n61) {$false$};
\node at (\rS, -\distance) (n62) {$false$};
\node at (\rS, -2*\distance) (n63) {$false$};
\node at (\rS, -3*\distance) (n64) {$true$};
% second part in 6
\node at (\rS, -7*\distance) (n65) {$false$};
\node at (\rS, -8*\distance) (n66) {$true$};
\node at (\rS, -9*\distance) (n67) {$true$};
\node at (\rS, -10*\distance) (n68) {$true$};
\node at (\rS, -11*\distance) (n69) {$true$};

\def\rF{\rS - 1.5}
\def\dH{\distance / 2}

\node at (\rF, -\dH) (n51) {$false$};
\node at (\rF, -3 * \dH) (n52) {$false$};
\node at (\rF, -5 * \dH) (n53) {$x_5$};
% first gap in 5
\node at (\rF, -8 * \dH) (n54) {$false$};
\node at (\rF, -10 * \dH) (n55) {$true$};
\node at (\rF, -12 * \dH) (n56) {$true$};
% second gap in 5
\node at (\rF, -15 * \dH) (n57) {$x_5$};
\node at (\rF, -17 * \dH) (n58) {$true$};
\node at (\rF, -19 * \dH) (n59) {$true$};
\node at (\rF, -21 * \dH) (n510) {$true$};

\def\rFF{\rF - 2}
\node at (\rFF, -\distance) (n41) {$false$};
\node at (\rFF, -2*\distance) (n42c) {$\left( x_4 \land x_5 \right)$};

\node at (\rFF, -4.5*\distance) (n43) {$x_4$};
\node at (\rFF, -5.5*\distance) (n44) {$true$};

\node at (\rFF, -8*\distance) (n45c) {$x_4 \lor x_5$};
\node at (\rFF, -9*\distance) (n46) {$true$};
\node at (\rFF, -10*\distance) (n47) {$true$};

\def\rT{\rFF - 2.8}
\node at (\rT, -1.5*\distance) (n31c) {$\left( x_3 \land x_4 \land x_5 \right)$};
\node at (\rT, -5*\distance) (n32c) {$x_3 \lor x_4$};
\node at (\rT, -8.5*\distance) (n33c) {$x_3 \lor x_4 \lor x_5$};
\node at (\rT, -9.5*\distance) (n34) {$true$};
% end uncover
}
\uncover<2->
{
\def\rTT{\rT - 2.8}
\node at (\rTT, -2*\distance) (n21c1) {\only<2>{\textcolor{blue}}{$\left( x_2 \land x_3 \right) \lor$}};
\node at (\rTT, -3*\distance) (n21c2) {\only<2>{\textcolor{blue}}{$\left( x_2 \land x_4 \right) \lor$}};
\node at (\rTT, -4*\distance) (n21c3) {\only<2>{\textcolor{blue}}{$\left( x_3 \land x_4 \land x_5 \right)$}};
}
\uncover<3->
{
\node at (\rTT, -8.5*\distance) (n22c1) {\only<3>{\textcolor{blue}}{$x_2 \lor x_3\ \lor$}};
\node at (\rTT, -9.5*\distance) (n22c2) {\only<3>{\textcolor{blue}}{$x_4 \lor x_5$}};
% end uncover
}

\def\rO{\rTT - 2.9}
\node at (\rO, -2.5*\distance) (n11) {$\only<3>{\textcolor{blue}}{\left(x_1 \land x_2\right)}
\lor$};
\node at (\rO, -3.5*\distance) (n11c) {$\only<3>{\textcolor{blue}}{\left( x_1 \land x_3\right)}
\lor$};
\node at (\rO, -4.5*\distance) (n11c1) {$\only<3>{\textcolor{blue}}{\left(x_1 \land x_4\right)}
\lor$};
\node at (\rO, -5.5*\distance) (n11c2) {$\only<3>{\textcolor{blue}}{\left(x_1 \land x_5\right)}
\lor$};
\node at (\rO, -6.5*\distance) (n11c3) {$\only<2>{\textcolor{blue}}{\left( x_2 \land x_3 \right)}
\lor$};
\node at (\rO, -7.5*\distance) (n11c4) {$\only<2>{\textcolor{blue}}{\left( x_2 \land x_4 \right)}
\lor$};
\node at (\rO, -8.5*\distance) (n11c5) {$\only<2>{\textcolor{blue}}{\left( x_3 \land x_4 \land x_5 \right)}$};

\def\spacing{0.25}
\def\yTop{0.5}
\def\yBot{-11.5*\distance}

\foreach \xPos in {\rT, \rTT, \rFF, \rF, \rS}
{
	\draw (\xPos - \spacing, \yTop) -- (\xPos - \spacing, \yBot);
}

\uncover<4->
{
\draw (\rT - \spacing, -6.5*\distance)--(\rS - \spacing + 1.5, -6.5*\distance);
\draw (\rFF - \spacing, -3.5*\distance)--(\rS - \spacing + 1.5, -3.5*\distance);
}

\begin{pgfonlayer}{background}
\uncover<4->
{
%\draw[fill=shadecolor, draw=shadecolor] (n33c.north west) rectangle (n34.south east);

%\draw[fill=shadecolor, draw=shadecolor] (n41.north west) rectangle (n42c.south east);
%\draw[fill=shadecolor, draw=shadecolor] (n42c.south west) rectangle (n41.north east);

%\draw[fill=shadecolor, draw=shadecolor] (n43.north west) rectangle (n44.south east);
%\draw[fill=shadecolor, draw=shadecolor] (n44.south west) rectangle (n43.north east);
%\draw[fill=shadecolor, draw=shadecolor] (n45c.north west) rectangle (n47.south east);

%\draw[fill=shadecolor, draw=shadecolor] (n51.north west) rectangle (n53.south east);
%\draw[fill=shadecolor, draw=shadecolor] (n57.north west) rectangle (n510.south east);
%\draw[fill=shadecolor, draw=shadecolor] (n510.south west) rectangle (n57.north east);
}
\end{pgfonlayer}

\end{tikzpicture}
}
\end{center}

\end{frame}

%\begin{frame}
%\frametitle{Decomposing a DNF: Example}
%\begin{example}
%Consider $\phi\equiv(x_1\land x_2)\lor(x_1\land
%x_3)\lor(x_1\land x_4)\lor(x_1\land x_5)\lor(x_2\land x_3)\lor(x_2\land x_4)\lor(x_3\land x_4\land x_5)$.
%
%We have $\ell=1$ and thus $X = \{x_1\}$.
%
%To find an LPB for $\phi$ we must find LPBs for\\
%$\Cut{\phi}{\{x_1\}}{0}$ \only<1>{$\equiv (x_2 \land x_3) \lor (x_2 \land x_4) \lor (x_3 \land x_4 \land x_5)$}\only<2->{ represented by $3x_2 + 2 x_4 + 2x_3 + x_5 \geq$}\only<2>{ $5$}\only<3->{ $(4, 5]$} \\
%and\\
%$\Cut{\phi}{\{x_1\}}{1}$\only<1>{$\equiv x_2 \lor x_3 \lor x_4 \lor x_5$} \only<2->{ represented by $ 3x_2 + 2 x_4 + 2x_3 + x_5 \geq$}\only<2>{ $1$}\only<3->{ $(0, 1]$}
%
%\uncover<2->{Thus, $\phi$ can be represented by $4x_1 + 3x_2 + 2x_3 + 2x_4 + x_5 \geq$}
%\only<2>{$5$}\only<3->{$(4, 5]$}
%\end{example}
%\end{frame}

%\subsection{Composing LPBs}
\begin{frame}[squeeze]{Composing LPBs}
\scalebox{0.55}
{
\begin{tikzpicture}[node distance=.25cm, every node/.style={anchor=west}]
\def\rS{0}
\def\distance{0.7cm}

\node at (\rS, 0) (n61) {$\inter{\only<2, 8>{\textcolor{blue}}{0}}{\only<5, 9>{\textcolor{blue}}{\infty}}$};
\node at (\rS, -\distance) (n62) {$\inter{\only<3, 5, 8>{\textcolor{blue}}{0}}{\only<2, 6, 9>{\textcolor{blue}}{\infty}}$};
\node at (\rS, -2*\distance) (n63) {$\inter{\only<4, 6>{\textcolor{blue}}{0}}{\only<3, 7>{\textcolor{blue}}{\infty}}$};
\node at (\rS, -3*\distance) (n64) {$\inter{\only<7>{\textcolor{blue}}{-\infty}}{\only<4>{\textcolor{blue}}{0}}$};
% second part in 6
\node at (\rS, -7*\distance) (n65) {$\inter{0}{\infty}$};
\node at (\rS, -8*\distance) (n66) {$\inter{-\infty}{0}$};
\node at (\rS, -9*\distance) (n67) {$\inter{-\infty}{0}$};
\node at (\rS, -10*\distance) (n68) {$\inter{-\infty}{0}$};
\node at (\rS, -11*\distance) (n69) {$\inter{-\infty}{0}$};

\def\rF{\rS - 3.5}
\def\dH{\distance / 2}
\uncover<2->
{
\node at (\rF, -\dH) (n51) {$\only<2-7>{\inter{?}{?}}\only<8->{\inter{ \only<8>{\textcolor{blue}}{1}}{\only<9>{\textcolor{blue}}{\infty}}}$};
\node at (\rF, -3 * \dH) (n52) {$\only<2-7>{\inter{?}{?}}\only<8->{\falseInt{1}}$};
\node at (\rF, -5 * \dH) (n53) {$\only<2-7>{\inter{?}{?}}\only<8->{\inter{0}{1}}$};
% first gap in 5
\node at (\rF, -8 * \dH) (n54) {$\only<2-7>{\inter{?}{?}}\only<8->{\falseInt{1}}$};
\node at (\rF, -10 * \dH) (n55) {$\only<2-7>{\inter{?}{?}}\only<8->{\trueInt}$};
\node at (\rF, -12 * \dH) (n56) {$\only<2-7>{\inter{?}{?}}\only<8->{\trueInt}$};
% second gap in 5
\node at (\rF, -15 * \dH) (n57) {$\only<2-7>{\inter{?}{?}}\only<8->{\inter{0}{1}}$};
\node at (\rF, -17 * \dH) (n58) {$\only<2-7>{\inter{?}{?}}\only<8->{\trueInt}$};
\node at (\rF, -19 * \dH) (n59) {$\only<2-7>{\inter{?}{?}}\only<8->{\trueInt}$};
\node at (\rF, -21 * \dH) (n510) {$\only<2-7>{\inter{?}{?}}\only<8->{\trueInt}$};
}

\uncover<10->
{
\def\rFF{\rF - 3.4}
\node at (\rFF, -\distance) (n41) {$\falseInt{3}$};
\node at (\rFF, -2*\distance) (n42) {$\inter{2}{3}$};
\node at (\rFF, -2.7*\distance + 10.5) (n42c) {};
\node at (\rFF, -4.5*\distance) (n43) {$\inter{1}{2}$};
\node at (\rFF, -5.5*\distance) (n44) {$\trueInt$};

\node at (\rFF, -8*\distance) (n45) {$\inter{0}{1}$};
\node at (\rFF, -8.2*\distance) (n45c) {};
\node at (\rFF, -8.9*\distance) (n46) {$\trueInt$};
\node at (\rFF, -9.9*\distance) (n47) {$\trueInt$};

\def\rT{\rFF - 3.2}
\node at (\rT, -1.5*\distance) (n31) {$\inter{4}{5}$};
\node at (\rT, -2.2*\distance + 10.5) (n31c) {};
\node at (\rT, -5*\distance) (n32) {$\inter{1}{2}$};
\node at (\rT, -5.3*\distance) (n32c) {};
\node at (\rT, -8.5*\distance) (n33) {$\inter{0}{1}$};
\node at (\rT, -8.7*\distance) (n33c) {};
\node at (\rT, -9.5*\distance) (n34) {$\trueInt$};

\def\rTT{\rT - 3}
\node at (\rTT, -4*\distance + 10.5) (n21) {\only<2>{\textcolor{blue}}{$\inter{4}{5}$}};
\node at (\rTT, -2*\distance + 10.5) (n21c1) {};
\node at (\rTT, -2.7*\distance + 10.5) (n21c2) {};
\node at (\rTT, -3.4*\distance + 10.5) (n21c3) {};

\node at (\rTT, -9*\distance) (n22) {\only<3>{\textcolor{blue}}{$\inter{0}{1}$}};
\node at (\rTT, -8.8*\distance) (n22c1) {};
\node at (\rTT, -9.5*\distance) (n22c2) {};
% end uncover

\def\rO{\rTT - 3.75}
\node at (\rO, -6.5*\distance) (n11) {$\inter{4}{5}$};
% end uncover
}

\def\spacing{0.25}
\def\yTop{2.125}
\def\yBot{-11.5*\distance}

\foreach \xPos in {\rT, \rTT, \rFF, \rF, \rS}
{
	\draw (\xPos - \spacing, \yTop) -- (\xPos - \spacing, \yBot);
}

\def\xend{\rS - \spacing + 2}
\draw (\rT - \spacing, -6.5*\distance)--(\xend, -6.5*\distance);
\draw (\rFF - \spacing, -3.5*\distance)--(\xend, -3.5*\distance);

%\begin{pgfonlayer}{background}
%\uncover<12->
%{
%\draw[fill=shadecolor, draw=shadecolor] (n33.north west) rectangle (n34.south east);

%\draw[fill=shadecolor, draw=shadecolor] (n41.north west) rectangle (n42.south east);
%\draw[fill=shadecolor, draw=shadecolor] (n42.south west) rectangle (n41.north east);

%\draw[fill=shadecolor, draw=shadecolor] (n43.north west) rectangle (n44.south east);
%\draw[fill=shadecolor, draw=shadecolor] (n44.south west) rectangle (n43.north east);
%\draw[fill=shadecolor, draw=shadecolor] (n45.north west) rectangle (n47.south east);
%}

%\uncover<2->
%{
%\draw[fill=shadecolor, draw=shadecolor] (n51.north west) rectangle (n53.south east);
%\draw[fill=shadecolor, draw=shadecolor] (n53.south west) rectangle (n51.north east);


%\draw[fill=shadecolor, draw=shadecolor] (n57.north west) rectangle (n510.south east);
%\draw[fill=shadecolor, draw=shadecolor] (n510.south west) rectangle (n57.north east);
%}
%\end{pgfonlayer}

% sums above the table
\def\sumY{0.5}
\def\xDist{3}
\def\rSS{\rS - \xDist}

% sums above the table
\draw (\rO - 0.5, \sumY) -- (\xend, \sumY);
\draw ($(\rO - 0.5, \sumY)+(0, 0.15)$) -- ($(\xend, \sumY)+(0, 0.15)$);

\node at ($(\rS, \sumY)+(0, 0.5)$) {$0 \geq \dots$};
\uncover<8->
{
\node at ($(\rF, \sumY)+(0, 0.5)$) {$1x_5 \geq \dots$};
}

\uncover<10->
{
\node at ($(\rFF, \sumY)+(0, 0.5)$) {$2x_4 + x_5 \geq \dots$};

\node at ($(\rT, \sumY)+(0, 0.5)$) {$2x_4 + x_5 \geq \dots$};
\node at ($(\rT, \sumY)+(0, 1)$) {$2x_3 +\text{ }$};

\node at ($(\rTT, \sumY)+(0, 0.5)$) {$2x_4 + x_5 \geq \dots$};
\node at ($(\rTT, \sumY)+(0, 1)$) {$3x_2 + 2x_3 + \text{ }$};

\node at ($(\rO, \sumY)+(0, 0.5)$) {$2x_4 + x_5 \geq \dots$};
\node at ($(\rO, \sumY)+(0, 1)$) {$4x_1 + 3x_2 + 2x_3 + \text{ }$};
}
\end{tikzpicture}
}

\begin{overlayarea}{\textwidth}{3cm}

\only<2-7>
{
Choose coefficient $a_5$ s.\,t.
\vspace{-0.3cm}
\begin{align*}
&\max \left\lbrace
\only<2>{\textcolor{blue}}{0 - \infty},
\only<3>{\textcolor{blue}}{0 - \infty},
\only<4>{\textcolor{blue}}{0 - 0},
0 - 0,
-\infty - 0,
-\infty - 0,
-\infty - 0
\right\rbrace < a_5 <\\
&\min \left\lbrace
\only<5>{\textcolor{blue}}{\infty - 0},
\only<6>{\textcolor{blue}}{\infty - 0},
\only<7>{\textcolor{blue}}{\infty - -\infty},
\infty - -\infty,
0 - -\infty,
0 - -\infty,
0 - -\infty
\right\rbrace
\end{align*}

\uncover<7>
{
\vspace{-0.4cm}
i.\,e. $0 < a_5 < \infty \Rightarrow a_5 = 1$
}
}


\only<8-9>
{
$s_{\phi'} = \max\left\lbrace \only<10>{\textcolor{blue}}{0}, \only<10>{\textcolor{blue}}{0} + 1 \right\rbrace = 1$, $b_{\phi'} = \min\left\lbrace \only<11>{\textcolor{blue}}{\infty}, \only<11>{\textcolor{blue}}{\infty} + 1 \right\rbrace = \infty$
}

%\only<12>
%{
%choose $a_4$ s.\,t.
%\begin{align*}
%&\max\left\lbrace 1- \infty, 1-\infty, 1-0, \;\; 1-1 \right\rbrace < a_4 <\\
%&\min\left\lbrace \infty - 1, \infty - 1, \infty --\infty, \;\; \infty - 0  \right\rbrace
%\end{align*}
%i.\,e. $1 < a_4 < \infty \Rightarrow a_4 = 2$.
%}

\uncover<10->
{
We have to choose $d \in \inter{4}{5} \Rightarrow d = 5$.
% TODO: have to oder must?
We obtain the LPB
\begin{align*}
4x_1 + 3x_2 + 2x_3 + 2x_4 + 1x_5 \geq 5
\end{align*}
}

\end{overlayarea}
\end{frame}


\subsection{Incompleteness}
\begin{frame}
\frametitle{How to Choose the Coefficient?}
\begin{itemize}
\item We always have to choose $a_{k+1}$ within certain limits.
\item Can a ``bad choice'' of a coefficient lead to a dead end later?
  \pause
\item 
\cite{WenzelmannBachelor11} found by experimentation: yes, proving 
\cite{Sma-CPAIOR07} wrong. 
\item
\cite{CoaLew61} were already aware of this. \pause
\item 
One of the simplest examples: 
\begin{align*}
\phi \equiv& \left( x_1 \land x_2 \right) \lor \left( x_1 \land x_3 \right) \lor \left(x_1 \land x_4 \land x_5\right) \lor \left(x_2 \land x_3 \land x_4\right) \lor\\
& \left(x_2 \land x_3 \land x_5 \right) \lor \left( x_2 \land x_4 \land x_5 \right) \lor \left( x_3 \land x_4 \land x_5 \land x_6 \right)
\end{align*}
represented by
\begin{align*}
9x_1 + 7x_2 + 6x_3 + 4x_4 + 4x_5 + x_6 \geq 15
\end{align*}
\end{itemize}
\end{frame}


\begin{frame}{The ``repair'' Procedure}
Based on \cite{CoaLew61}, we have implemented a ``repair''
(``backtracking'') procedure \ldots
\end{frame}


\begin{frame}{The Idea of ``repair''}
Rather than just siblings, look at ``cousins'' etc. 

{\scriptsize
\begin{center}
\begin{tabular}{r|r|r|r|r|r}
\hspace{2cm}&\hspace{2cm}  &     $2x_3+2x_4$    &        $2x_4+$            &                      & $\sum_{i=6}^5a_ix_i$ \\
       &               & $1x_5\geq\ldots$               &  $1x_5\geq\ldots$               &   $1x_5\geq\ldots$             &  $\geq\ldots$    \\\hline\hline
&                      &                      &                             & \ld{$\LPBT{x_{3..4}}{0}\threshold{1}{\infty}$} & $\LPBT{x_{3..5}}{0}\threshold{0}{\infty}$\\
&$\LPBT{x_1}{0}$        & $\LPBT{x_2}{0}$      & \sd{$\LPBT{x_{3}}{0}\threshold{3}{\infty}$}     & \ld{$\LPBT{x_{3..4}}{1}\threshold{1}{\infty}$} & $\LPBT{x_{3..5}}{1}\threshold{0}{\infty}$ \\
&                     & \ub{$\threshold{4}{5}$}         & \sd{$\LPBT{x_{3}}{1}\threshold{2}{3}$}      &  \ld{$\LPBT{x_{3..4}}{2}\threshold{0}{1}$} & $\LPBT{x_{3..5}}{2}\threshold{0}{\infty}$ \\
&                                &                      &                                 &                         &  $\LPBT{x_{3..5}}{3}\threshold{-\infty}{0}$\\\cline{4-6}
&                     & $\LPBT{x_2}{1}$    & \ld{$\LPBT{x_{3}}{0}\threshold{1}{2}$}      & $\LPBT{x_{3..4}}{0}\threshold{1}{\infty}$ & \\
&                     & \textcolor{blue}{$\threshold{1}{2}$}& \ld{$\LPBT{x_{3}}{1}\threshold{-\infty}{0}$}       & $\LPBT{x_{3..4}}{1}\threshold{-\infty}{0}$ & \\
                                             &     &     &                                 & $\LPBT{x_{3..4}}{2}\threshold{-\infty}{0}$ & \\\cline{3-6}
&&&&&\\[-2.7ex]                   
&                     &                    &                                 & \ld{$\LPBT{x_{3..4}}{0}\threshold{0}{1}$} &$\LPBT{x_{3..5}}{0}\threshold{0}{\infty}$ \\
&$\LPBT{x_1}{1}$       &                    &\sd{$\LPBT{x_{3}}{0}\threshold{0}{1}$}      & \ld{$\LPBT{x_{3..4}}{1}\threshold{-\infty}{0}$} &$\LPBT{x_{3..5}}{1}\threshold{-\infty}{0}$ \\
&                                &\ud{$\LPBT{x_2}{0}\threshold{0}{1}$}& \sd{$\LPBT{x_{3}}{1}\threshold{-\infty}{0}$}       & \ld{$\LPBT{x_{3..4}}{2}\threshold{-\infty}{0}$} &$\LPBT{x_{3..5}}{2}\threshold{-\infty}{0}$ \\
&                     &\textcolor{blue}{\ud{$\LPBT{x_2}{1}\threshold{-\infty}{0}$}}& \sd{$\LPBT{x_{3}}{2}\threshold{-\infty}{0}$}   & \ld{$\LPBT{x_{3..4}}{3}\threshold{-\infty}{0}$} & $\LPBT{x_{3..5}}{3}\threshold{-\infty}{0}$\\
&                     &                   &                                &                    &$\LPBT{x_{3..5}}{4}\threshold{-\infty}{0}$
\end{tabular}
\end{center}}
Enforces $1-0<a_1<2--\infty$. One might discover contradictions.  
\end{frame}


\begin{frame}{Remarks}
\begin{enumerate}
\item 
Does it correspond precisely to \cite{CoaLew61}?\pause
\item 
Our current implementation is still incomplete. \pause
\item 
Taken to the extreme, we get at least the linear program.\pause
\item
In \cite{CoaLew61} it is conjectured that the basic procedure
is complete up to about $m=9$; in reality already for $m=6$. \pause
\item
Dozen rounds of extending our code. \pause
\item
Constant effort per column. \pause
\item
Combinatorial algorithm may require
several calls to ``repair''.
\end{enumerate}
\end{frame}


\section{Experimental Results}


\begin{frame}{Implementation and Experiments}
\begin{itemize}
\item 
Both algorithms were implemented in C++.
\item 
To test, we generated DNFs of which we knew that they represent
threshold functions: 
  \begin{itemize}
  \item For up to $m=7$, all 28262 instances;
  \item For $m=8$,  248k instances (10\%);
  \item For bigger $m$, a ``random'' sample, from 30000 instances for $m=10$ to
    just 60 for $m=22$. 
  \end{itemize}
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Failure Rate of Current Implementation in \%}
\begin{tikzpicture}
\begin{semilogyaxis}[width=11cm,height=7cm,%xlabel=dimension,ylabel=Failure rate in \%,
ytick={0.01,0.1,1,10},
ymax=100]
\addplot[mark=*] coordinates {
(4,0.0001)
(5,0.0001)
(6,0.0001)
(7,0.0001)
(8,0.0141)
(9,0.01)
(10,0.05)
(11,0.167)
(12,0.533)
(13,0.767)
(14,0.7)
(15,2.4)
(16,1.333)
(17,3)
(18,2)
(19,4.33333)
(20,11.3333)
(21,13.3333)
(22,18.3333)
(23,5)
}; 
%\addlegendentry{Failure rate}
\end{semilogyaxis}
\end{tikzpicture}  
\end{frame}


\begin{frame}
\frametitle{Percentage of the Successful Calls
  Requiring ``repair''}
\begin{tikzpicture}
\begin{axis}[width=11cm,height=7cm,%xlabel=dimension,ylabel=\% requiring repair,
ymax=20]
%\addplot[mark=*] coordinates {
%(4,100)
%(5,100)
%(6,99.195)
%(7,91.565)
%(8,94.4)
%(9,99.1)
%(10,98.743)
%(11,97.5)
%(12,96.7)
%(13,94.067)
%(14,94.533)
%(15,89.067)
%(16,94)
%(17,84.6667)
%(18,88.3333)
%(19,90)
%(20,80.3333)
%(21,80)
%(22,73.3333)
%(23,80)
%}; 
%\addlegendentry{Success rate without need for repair}
\addplot[mark=x] coordinates {
(4,0)
(5,0)
(6,0.805)
(7,8.435)
(8,5.578)
(9,0.89)
(10,1.207)
(11,2.33)
(12,2.767)
(13,5.167)
(14,4.767)
(15,8.533)
(16,4.66667)
(17,12.3333)
(18,9.66667)
(19,5.66667)
(20,8.333333)
(21,6.66667)
(22,8.33333)
(23,15)
}; %\addlegendentry{Requiring repair}
\end{axis}
% \begin{axis}...\end{axis} for normal plots,
% \begin{semilogxaxis}...\end{semilogxaxis} for plots which have a normal y axis and a logarithmic x axis,
% \begin{semilogyaxis}...\end{semilogyaxis} the same with x and y switched,
% \begin{loglogaxis}...\end{loglogaxis} for double$(G!9(Blogarithmic plots.
\end{tikzpicture}
\end{frame}


\begin{frame}
\frametitle{Runtime in ms}
\begin{tikzpicture}
\begin{semilogyaxis}[legend
  style={at={(0.53,0.95)}},width=11cm,height=7cm,%xlabel=dimension,%
%ylabel={Runtime ms, \#.~var.~occurr.},
ymax=10000000]
\addplot[mark=triangle] coordinates {
(4,0.01)
(5,0.01)
(6,0.05)
(7,0.08)
(8,0.124)
(9,0.224)
(10,0.370)
(11,0.691)
(12,1.149)
(13,2.157)
(14,3.545)
(15,7.292)
(16,11.622)
(17,28.488)
(18,45.476)
(19,98.432)
(20,171.278)
(21,553.077)
(22,1455.92)
(23,2104.04)
}; 
%\addlegendentry{Combin.~alg.}%No repair necessary
%\addplot[mark=x] coordinates {
%(4,0.1)
%(5,0.1)
%(6,0.1)
%(7,0.1)
%(8,0.2)
%(9,0.3)
%(10,0.5)
%(11,1.1)
%(12,1.1)
%(13,1.7)
%(14,3.4)
%(15,4.0)
%(16,3.5)
%(17,11.4)
%(18,27.9)
%(19,12.9)
%(20,98.4)
%}; \addlegendentry{Repair needed}
%	\addplot+[smooth,mark=*,mark size=1pt] file {input.dat}; \addlegendentry{file input}
\addplot[mark=star] coordinates {
(4,0.1)
(5,0.2)
(6,0.2)
(7,0.3)
(8,0.3)
(9,0.5)
(10,0.8)
(11,1.4)
(12,2.3)
(13,6.4)
(14,10.0)
(15,24.0)
(16,34.2)
(17,97.4)
(18,262.1)
(19,897.3)
(20,2178.2)
(21,12271.8)
(22,29291.5)
%(23,)
}; %\addlegendentry{LP alg.}
%\addplot[mark=o] coordinates {
%(4,3.29)
%(5,5.09)
%(6,8.13)
%(7,13.18)
%(8,20.85)
%(9,40.16)
%(10,59.81)
%(11,101.57)
%(12,148.5)
%(13,266.89)
%(14,387.68)
%(15,683.66)
%(16,1018.9)
%(17,2005.45)
%(18,2723.27)
%(19,4926.82)
%(20,6406.7)
%(21,17388.7)
%(22,22239.82)
%(23,36524.78)
%}; \addlegendentry{\# clauses per DNF}
\addplot[mark=o] coordinates {
(4,7.04)
(5,13.08)
(6,24.39)
(7,45.34)
(8,69.64)
(9,179.11)
(10,293.07)
(11,550.51)
(12,871.7)
(13,1710.76)
(14,2667.24)
(15,5052.25)
(16,8039.12)
(17,16885.9)
(18,24264.3)
(19,46262.8)
(20,63234.13)
(21,181538)
(22,243303)
(23,418208.7)
}; 
%\addlegendentry{Input size}%No repair necessary
\legend{
Comb.~alg.,
LP alg.,
Input size
};
\end{semilogyaxis}
% \begin{axis}...\end{axis} for normal plots,
% \begin{semilogxaxis}...\end{semilogxaxis} for plots which have a normal y axis and a logarithmic x axis,
% \begin{semilogyaxis}...\end{semilogyaxis} the same with x and y switched,
% \begin{loglogaxis}...\end{loglogaxis} for double$(G!9(Blogarithmic plots.
\end{tikzpicture}
\end{frame}

\begin{frame}{Conclusion}
\begin{itemize}
\item 
Presented implementations  of two algorithms for the
threshold recognition problem:
  \begin{itemize}
  \item Translation to LP
  \item Combinatorial
  \end{itemize}
\end{itemize}

Future work: 
\begin{itemize}
\item
Heuristics for guessing the right coefficient, reducing need for
``repair''.
\item
Make algorithm complete by making ``repair'' perfect. 
\end{itemize}
  
\end{frame}



\begin{frame}[allowframebreaks]
\frametitle{References}
\bibliography{smaus,own_publications}
%\bibliographystyle{plainnat}
\bibliographystyle{unsrtnat}
%\bibliography{plainnat}
\end{frame}
\end{document}